perm filename OPTIM[EKL,SYS] blob
sn#821261 filedate 1986-07-29 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00029 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00004 00002 functions as lists of numbers
C00006 00003 functions as lists of numbers
C00009 00004 a list of elementary facts
C00011 00005 a list of the lemmata and theorems proved
C00013 00006 application to functions
C00015 00007 a list of the theorems and lemmata proved
C00017 00008 corollaries
C00019 00009 *-- proofs: condition for def_appl
C00021 00010 the application of the pigeon hole
C00022 00011 lemma sortcomp
C00023 00012 lemma length_compose
C00029 00013 lemmata nth_compose, nthcdr_compose
C00032 00014 theorem 1(i): perm compose
C00038 00015 theorem 1(ii): associativity of compose
C00043 00016 id uniqueness
C00044 00017 theorem 2(i):id implies perm
C00045 00018 theorem 2(ii):identity right
C00047 00019 theorem 2(iii):identity left
C00049 00020 lemma inv implies into
C00051 00021 theorem 3(i):inv implies perm
C00054 00022 theorem 3(ii):inverse_right
C00057 00023 theorem 3(iii):inverse left
C00062 00024 application: sorts of the other functions
C00063 00025 length ident and lengthinverse
C00066 00026 id main
C00069 00027 theorem 2 as corollary
C00070 00028 inv main
C00073 00029 theorem 3 as corollary
C00077 ENDMK
C⊗;
;functions as lists of numbers
(wipe-out)
(get-proofs appl prf ekl sys)
;definitions of composition,identity, inverse as predicates
(proof comp_pred)
;composition of functions
(decl (comp) (type: |ground⊗ground⊗ground→truthval|) (syntype: constant)
(bindingpower: 930))
(define comp |∀u v w.comp(u,v,w)≡
length u=length w∧(∀n.n<length u⊃nth(u,n)=nth(v,nth(w,n)))|)
(label compdef)
;the identity function
(decl (id) (type: |ground→truthval|))
(defax id |∀u.id(u)≡(∀n.n<length u⊃nth(u,n)=n)|)
(label id_def)
;the inverse of a function
(decl (inv) (type: |ground⊗ground→truthval|))
(defax inv |∀u v.inv(u,v)≡(∀n.n<length u⊃nth(u,n)=fstposition(v,n))|)
(label invdef)
;functions as lists of numbers
;definitions of composition,identity, inverse as functions
(proof comp_fnct)
;the condition for λx.appl(v,x) to be defined on u as domain is that u satisfies
;allp(λx.natnum(x)∧x<length(v),u)
(decl def_appl (type: |@u⊗@u→truthval|))
(define def_appl |∀u v.def_appl(v,u)≡allp(λx.natnum(x)∧x<length(v),u)|)
(label def_appl_fact)
;composition of functions
(decl (compose) (infixname: |⊗|) (type: |ground⊗ground→ground|) (syntype: constant)
(bindingpower: 930))
(define compose |∀u v x.(u⊗nil)=nil∧
(u⊗(x.v))=(nth(u,x)).(u⊗v)|listinductiondef)
(label composedef)
;the identity function
(decl (ident1) (type: |ground⊗ground→ground|))
(defax ident1 |∀x u n i.ident1(i,0)=nil∧
ident1(i,n')=i.ident1(i',n)|)
(label identdef1)
(decl (ident) (type: |ground→ground|))
(define ident |∀n.ident(n)=ident1(0,n)|)
(label identdef)
;the inverse of a function
(decl (invers1) (type: |ground⊗ground⊗ground→ground|))
(defax invers1 |∀u i n.invers1(u,i,0)=nil∧invers1(nil,i,n)=nil∧
invers1(u,i,n')=if null(fstposition(u,i)) then nil
else fstposition(u,i).invers1(u,i',n)|)
(label inversdef1)
(decl (inverse) (type: |ground→ground|))
(define inverse|∀u.inverse(u)=invers1(u,0,length(u))|)
(label inversdef)
;a list of elementary facts
(proof permfacts)
;conditions for def_appl
(axiom |∀u v.into(u)∧length(u)≤length(v)⊃def_appl(v,u)|)
(label def_appl_condition)
(axiom |∀u v.perm u∧length u = length v⊃def_appl(v,u)|)
(label def_appl_condition1)
;facts about sorts
;compose
(axiom |∀v u.def_appl(v,u)⊃listp v⊗u|)
(label sortcomp)(label simpinfo)
(axiom |∀v u.allp(λx.natnum(x)∧x<length v,u)⊃listp v⊗u|)
(label simpinfo)
;a fact about the length
;lemma length_compose
(axiom |∀w u.def_appl(w,u)⊃length(w⊗u)=length(u)|)
(label length_compose)
;a list of the lemmata and theorems proved
(proof comp)
;compose
;lemma nth_compose
(axiom |∀v u n.def_appl(v,u)∧n<length u⊃nth(v⊗u,n)=nth(v,nth(u,n))|)
(label nth_compose)
;theorem 1
(axiom |∀w v u.def_appl(w,v)∧def_appl(v,u)⊃(w⊗v)⊗u=w⊗(v⊗u)|)
(label assoc_comp)
;lemma perm_compose
(axiom |∀u v.perm(u)∧perm(v)∧length(u)=length(v)⊃perm(u⊗v)|)
(label perm_compose)
;identity
(axiom |∀u w.id(u)∧id(w)∧length u=length w⊃u=w|)
(label id_uniqueness)
(axiom |∀u.id(u)⊃perm(u)|)
(label id_perm)
(axiom |∀u w.id(u)∧length w=length u⊃w⊗u=w|)
(label id_right)
(axiom |∀u w.id(u)∧perm(w)∧length w=length u⊃w=u⊗w|)
(label id_left)
;inverse right
(axiom |∀u v w.perm(w)∧inv(u,w)∧length u=length w⊃id(w⊗u)|)
(label inv_right)
;inverse left
(axiom |∀u.perm(u)⊃inj(u)|)
(label perm_injectivity)
;for a proof of this, see the file mult[prm,glb]
;(axiom |∀u.perm(u)⊃(∀n.n<length u⊃fstposition(u,nth(u,n))=n)|)
;(label perm_fstposition_nth)
(axiom |∀u v.perm(u)∧inv(v,u)∧length v=length u⊃into(v)|)
(label inv_into)
(axiom |∀u v.perm(u)∧inv(v,u)∧length v=length u⊃perm(v)|)
(label inv_perm)
(axiom |∀u v w.perm(w)∧inv(u,w)∧length u=length w⊃id(u⊗w)|)
(label inv_left)
;application to functions
(proof permfacts)
;ident
(axiom |∀m n.listp ident1(m,n)|)
(label simpinfo)
(axiom |∀n.listp ident(n)|)
(label simpinfo)
;inverse
(axiom |∀u n i.listp invers1(u,i,n)|)
(label simpinfo)
(axiom |∀u.listp inverse(u)|)
(label simpinfo)
;facts about the length
;identity_length
(axiom |∀n m.length (ident1(m,n))=n|)
(label ident_length) (label simpinfo)
(axiom |∀n.length (ident(n))=n|)
(label simpinfo)
;inverse length
(axiom |∀u.perm u⊃length inverse(u)=length u|)
(label lengthinverse)
;a list of the theorems and lemmata proved
(proof permf)
;ident
;lemma id_main
(axiom |∀m n.n<m⊃nth(ident(m),n)=n|)
(label id_main)
;we prove it using the following fact
(axiom |∀m n.n<m⊃nthcdr(ident(m),n)=ident1(n,m-n)|)
(label id_main_part2)
(axiom |∀n.id ident(n)|)
(label id_ident)
;inverse
;lemma inv_main
(axiom |∀u n.perm u∧n<length(u)⊃nth(inverse(u),n)=fstposition(u,n)|)
(label inv_main)
;we prove this using the following fact
(axiom |∀u n.perm u∧n<length u⊃nthcdr(inverse(u),n)=invers1(u,n,length u-n)|)
(label inv_main_part2)
(axiom |∀u.perm u⊃inv(inverse u,u)|)
(label inv_inverse)
;corollaries
;theorem 2(i)
;theorem perm_ident
;∀N.PERM(IDENT(N))
;theorem 2(ii)
;identity_right_theorem
;∀U.U⊗IDENT(LENGTH U)=U
;theorem 2(iii)
;identity_left_theorem
;∀U.INTO(U)⊃IDENT(LENGTH U)⊗U=U
;theorem 3(i)
;theorem perm_inverse
;∀U.PERM(U)⊃PERM(INVERSE(U))
;theorem 3(ii)
;theorem compose_inverse_right
;∀U.PERM(U)⊃U⊗INVERSE U=IDENT(LENGTH U)
;theorem 3(ii)
;theorem compose_inverse_left
;∀U.PERM(U)⊃INVERSE U⊗U=IDENT(LENGTH U)
;*-- proofs: condition for def_appl
(assume |into u|)
(assume |length u≤length v|)
(rw -2 (open into))
;∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U
(trw |∀n.n<length u⊃natnum nth(u,n)∧nth(u,n)<length v| * (less_lesseq_fact1 -2))
;∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH V
(ue ((phi1.|λx.natnum x∧x<length v|)(u.u)) nth_allp *)
;ALLP(λX.NATNUM(X)∧X<LENGTH V,U)
(trw |def_appl(v,u)| (open def_appl) *)
;DEF_APPL(V,U)
(ci (-6 -5))
;INTO(U)∧LENGTH U≤LENGTH V⊃DEF_APPL(V,U)
(label def_appl_condition)
;a variant of the same condition
(rw def_appl_condition (open lesseq) (use normal mode: always))
;∀U V.(INTO(U)∧LENGTH U=LENGTH V⊃DEF_APPL(V,U))∧
; (INTO(U)∧LENGTH U<LENGTH V⊃DEF_APPL(V,U))
(derive |perm u∧length u = length v⊃def_appl(v,u)|
(def_appl_condition *)(open perm onto))
; ;the application of the pigeon hole
;
; (assume |perm u|)
;
; (rw * (open perm onto into))
; ;(∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U)∧
; ;(∀N.N<LENGTH U⊃MEMBER(N,U))
; ;deps: (15)
;
; (derive |(∀n.n<length u⊃fstposition(u,nth(u,n))=n)|
; (fstposition_nth perm_injectivity uniqueness_injectivity * -2))
;
; (ci -3)
; ;PERM(U)⊃(∀N.N<LENGTH U⊃FSTPOSITION(U,NTH(U,N))=N)
;lemma sortcomp
(unlabel simpinfo sortcomp)
(ue (phi |λu.def_appl(v,u)⊃listp v⊗u|) listinduction
(part 1 (open def_appl allp compose )))
;∀U.DEF_APPL(V,U)⊃LISTP V⊗U
(label simpinfo sortcomp)
;lemma length_compose
(proof length_compose)
(assume |def_appl(w,u)|)
(label l_c_1)
(rw * (open def_appl))
(label l_c_2)
;ALLP(λX.NATNUM(X)∧X<LENGTH W,U)
(assume |n<length(u)|))
(label l_c_3)
(ue ((u.u)(x.|nth(u,n)|)(phi1.|λx.natnum(x)∧x<length(w)|)) allp_elimination
nthmember sexp_nth l_c_3 l_c_2)
;NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH W
(label l_c_4)
(trw |sexp(nth(w,nth(u,n)))| sexp_nth l_c_4)
;SEXP NTH(W,NTH(U,N))
(label l_c_sort1)
(ci l_c_3)
;N<LENGTH U⊃SEXP NTH(W,NTH(U,N))
(label l_c_7)
(derive |allp(λX.NATNUM(X)∧X<LENGTH W,NTHCDR(U,N'))| (allp_nthcdr l_c_2))
;ALLP(λX.NATNUM(X)∧X<LENGTH W,NTHCDR(U,N'))
(derive |listp(w⊗nthcdr(u,n'))| (* sortcomp))
(label l_c_sort2)
(ci l_c_3)
;N<LENGTH U⊃LISTP W⊗NTHCDR(U,N')
(label l_c_8)
(ue ((phi.|λu.length(w⊗u)=length(u)|)(u.u)) nthcdr_induction
(part 1(open compose length )) l_c_7 l_c_8)
;LENGTH (W⊗U)=LENGTH U
(ci L_C_1)
;DEF_APPL(W,U)⊃LENGTH (W⊗U)=LENGTH U
;LEMMA
;DEF_APPL(W,U)⊃LENGTH (W⊗U)=LENGTH U
;Proof: by nthcdr_induction applied to U. For U = NIL, the result is given by the
;definition of compose. Assume LENGTH(W⊗NTHCDR(U,N'))=LENGTH(NTHCDR(U,N')), for N'
;less than LENGTH(U); want
;LENGTH(W⊗(NTH(U,N).NTHCDR(U,N'))=LENGTH(NTH(U,N).NTHCDR(U,N'))
;Since N is less than LENGTH(U), NTH(U,N) is an s-expression, so we can apply the
;definition of compose; the left hand side is
;LENGTH(NTH(W,NTH(U,N)).(W⊗NTHCDR(U,N')))
;so the inductive step will be proved if we show that, under the given assumption
;[line l_c_1], the terms are of the proper sorts. This is done as follows:
;Since W is defined as an application on U as domain [line l_c_1], NTH(U,N) is a
;natural number less than LENGTH(W). Therefore NTH(W,NTH(U,N)) is an s-expression
;[line l_c_sort1]. On the other hand, W is defined as an application on any part
;of U, since it is defined on U (using ALLP_NTHCDR) therefore W⊗NTHCDR(U,N') is
;a defined and is a list (using SORTCOMP).
;facts used:
;labels: LESS_LESSEQ_FACT1 (proof minus)
;∀N M K.N<M∧M≤K⊃N<K
;labels: SIMPINFO SEXP_NTH
;(AXIOM |∀U N.N<LENGTH U⊃SEXP NTH(U,N)|)
;labels: NTHMEMBER
;(AXIOM |∀U N.N<LENGTH U⊃MEMBER(NTH(U,N),U)|)
;labels: allp_elimination
;∀U.MEMBER(X,U)∧ALLP(PHI1,U)⊃PHI1(X)
;labels: ALLP_NTHCDR
;∀U N.ALLP(A,U)⊃ALLP(A,NTHCDR(U,N))
;labels: SIMPINFO SORTCOMP
;∀U.ALLP(λX.NATNUM(X)∧X<LENGTH V,U)⊃LISTP V⊗U
;labels: NTHCDR_INDUCTION
;(AXIOM |∀PHI U.PHI(NIL)∧
(∀N.N<LENGTH U⊃(PHI(NTHCDR(U,N'))⊃PHI(NTH(U,N).NTHCDR(U,N'))))⊃ PHI(U)|)
(show *)
;lemmata nth_compose, nthcdr_compose
(proof nth_compose)
;lemma nthcompose
;by double induction on n and u
;labels: DOUBLEINDUCTION1
;(∀U N X.PHI3(NIL,N)∧PHI3(U,0)∧(PHI3(U,N)⊃PHI3(X.U,N')))⊃(∀U N.PHI3(U,N))
;one base_case is proved by listinduction
(ue (phi |λu.¬null(u)∧def_appl(v,u)⊃nth(v⊗u,0)=nth(v,nth(u,0))|) listinduction
(part 1(open compose nth def_appl allp)) )
;∀U.¬NULL U∧DEF_APPL(V,U)⊃CAR (V⊗U)=NTH(V,CAR U)
(label a_c_base1)
;and the other is trivial; so
(ue (phi3 |λu n.def_appl(v,u)∧n<length(u)⊃nth(v⊗u,n)=nth(v,nth(u,n))|) doubleinduction1
(part 1(open compose def_appl allp)) a_c_base1)
;∀U N.DEF_APPL(V,U)∧N<LENGTH U⊃NTH(V⊗U,N)=NTH(V,NTH(U,N))
(label nth_compose)
; the similar fact for nthcdr is also easy
;nthcdr_compose
(ue (phi3 |λu n.n<length(u)∧def_appl(v,u)⊃nthcdr(v⊗u,n)=v⊗nthcdr(u,n)|) doubleinduction1
(part 1(open compose nthcdr def_appl allp)))
;∀U N.N<LENGTH U∧DEF_APPL(V,U)⊃NTHCDR(V⊗U,N)=V⊗NTHCDR(U,N)
(label nthcdr_comp1)
(trw |∀u v n.length(u)≤n∧def_appl(v,u)⊃length(v⊗u)≤n| length_compose)
(trw |∀u n.length(u)≤n∧def_appl(v,u)⊃nthcdr(v⊗u,n)=v⊗nthcdr(u,n)| *
(use trivial_nthcdr mode: always) (open compose))
;∀U N.LENGTH U≤N∧DEF_APPL(V,U)⊃NTHCDR(V⊗U,N)=V⊗NTHCDR(U,N)
(label nthcdr_comp2)
(derive |(p⊃r)∧(q⊃r)∧(p∨q)⊃r|)
(ue ((p.|length u≤n|)(q.|n<length u|)(r.|def_appl(v,u)⊃nthcdr(v⊗u,n)=v⊗nthcdr(u,n)|))
* nthcdr_comp2 nthcdr_comp1 trichotomy2)
;DEF_APPL(V,U)⊃NTHCDR(V⊗U,N)=V⊗NTHCDR(U,N)
;theorem 1(i): perm compose
(proof perm_compose)
1. (assume |perm u|)
(label pc1)
2. (assume |perm v|)
(label pc2)
3. (assume |length u = length v|)
(label pc3)
4. (rw pc2 (open perm onto))
(label pc4)
;INTO(V)∧(∀N.N<LENGTH V⊃MEMBER(N,V))
;deps: (PC2)
5. (ue ((u.v)(v.u)) def_appl_condition (open lesseq) pc3 pc4)
;DEF_APPL(U,V)
(label pc5)
;deps: (PC2 PC3)
6. (ue ((u.v)(w.u)) length_compose pc5)
;LENGTH (U⊗V)=LENGTH V
(label pc6)
;deps: (PC2 PC3)
7. (assume |n<length(u⊗v)|)
(label pc7)
8. (rw * (use pc6 mode: exact))
;N<LENGTH V
(label pc8)
;deps: (PC2 PC3 PC7)
9. (rw pc2 (open perm onto into))
;(∀N.N<LENGTH V⊃NATNUM(NTH(V,N))∧NTH(V,N)<LENGTH V)∧
;(∀N.N<LENGTH V⊃MEMBER(N,V))
(label pc9)
;deps: (PC2)
10. (derive |natnum(nth(v,n))∧nth(v,n)<length u| (pc8 *)
(use pc3 mode: exact))
(label pc10)
;deps: (PC2 PC3 PC7)
11. (rw pc1 (open perm onto into))
;(∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U)∧
;(∀N.N<LENGTH U⊃MEMBER(N,U))
(label pc11)
;deps: (PC1)
12. (ue (n |nth(v,n)|) * pc10)
;NATNUM(NTH(U,NTH(V,N)))∧NTH(U,NTH(V,N))<LENGTH U∧MEMBER(NTH(V,N),U)
(label pc12)
;deps: (PC1 PC2 PC3 PC7)
13. (derive |nth(u⊗v,n)=nth(u,nth(v,n))| (nth_compose pc5 pc8))
(label pc13)
;deps: (PC2 PC3 PC7)
14. (trw |natnum nth(u⊗v,n)∧nth(u⊗v,n)<length(u⊗v)| pc12
(use pc13 pc6 mode: exact)
(use pc3 mode: exact direction: reverse))
;NATNUM(NTH(U⊗V,N))∧NTH(U⊗V,N)<LENGTH (U⊗V)
;deps: (PC1 PC2 PC3 PC7)
15. (ci pc7)
;N<LENGTH (U⊗V)⊃NATNUM(NTH(U⊗V,N))∧NTH(U⊗V,N)<LENGTH (U⊗V)
;deps: (PC1 PC2 PC3)
16. (trw |into(u⊗v)| * (open into) pc5)
;INTO(U⊗V)
(label pc_into)
;deps: (PC1 PC2 PC3)
;part 2
17. (rw pc8 (use pc3 mode: exact direction: reverse))
;N<LENGTH U
(label pc20)
;deps: (PC2 PC3 PC7)
;labels: MEMBER_NTH
;∀U Y.MEMBER(Y,U)⊃(∃N.N<LENGTH U∧NTH(U,N)=Y)
18. (define jv |jv<length u ∧ nth(u,jv)=n| (* pc11 member_nth))
(label pc21)
;JV is unknown.
;the symbol JV is given the same declaration as J
;deps: (PC1 PC2 PC3 PC7)
19. (derive |jv<length v| * (use pc3 mode: exact direction: reverse))
;deps: (PC1 PC2 PC3 PC7)
20. (define kv |kv<length v ∧ nth(v,kv)=jv| (* pc9 member_nth))
(label pc22)
;KV is unknown.
;the symbol KV is given the same declaration as K
;deps: (PC1 PC2 PC3 PC7)
;labels: NTH_COMPOSE
;∀V U N.DEF_APPL(V,U)∧N<LENGTH U⊃NTH(V⊗U,N)=NTH(V,NTH(U,N))
21. (ue ((v.u)(u.v)(n.kv)) nth_compose pc5
(use * mode: always)(use pc21 mode: always))
(label pc23)
;NTH(U⊗V,KV)=N
;deps: (PC1 PC2 PC3 PC7)
22. (derive |kv<length(u⊗v)| (pc22 pc6))
;deps: (PC1 PC2 PC3 PC7)
;labels: NTHMEMBER
;∀U N.N<LENGTH U⊃MEMBER(NTH(U,N),U)
23. (trw |member(nth(u⊗v,kv),u⊗v)| (nthmember pc5 *))
;MEMBER(NTH(U⊗V,KV),U⊗V)
;deps: (PC1 PC2 PC3 PC7)
24. (rw * pc23)
;MEMBER(N,U⊗V)
;deps: (PC1 PC2 PC3 PC7)
25. (ci pc7)
;N<LENGTH (U⊗V)⊃MEMBER(N,U⊗V)
;deps: (PC1 PC2 PC3)
(label pc_onto)
26. (trw |perm(u⊗v)| (pc5 pc_into pc_onto) (open perm onto))
;PERM(U⊗V)
;deps: (PC1 PC2 PC3)
27. (ci (pc1 pc2 pc3))
;PERM(U)∧PERM(V)∧LENGTH U=LENGTH V⊃PERM(U⊗V)
(label perm_compose)
;theorem 1(ii): associativity of compose
(proof assoc_compose)
;associativity of compose
;by listinduction on u
(trw |def_appl(w,v)∧def_appl(v,u)⊃(w⊗v)⊗nil=w⊗(v⊗nil)|
(open compose ) sortcomp)
(label ass_comp_base)
(ue (phi |λu.def_appl(w,v)∧def_appl(v,u)⊃(w⊗v)⊗u=w⊗(v⊗u)|) listinduction
(part 1#2(open compose def_appl allp)) sortcomp ass_comp_base
(use nth_compose ue: ((v.w)(u.v)) ) )
;∀U.DEF_APPL(W,V)∧DEF_APPL(V,U)⊃(W⊗V)⊗U=W⊗(V⊗U)
(label assoc_comp)
;the conditions def_appl are satisfied
;if U and V are permutations of the same length
(trw |∀u v w.perm(v)∧perm(u)∧length v=length u∧length w=length u⊃
(w⊗v)⊗u=w⊗(v⊗u)| assoc_comp
(use def_appl_condition1 ue: ((u.u)(v.v)) )
(use def_appl_condition1 ue: ((u.v)(v.w)) ))
;∀U V W.PERM(V)∧PERM(U)∧LENGTH V=LENGTH U∧LENGTH W=LENGTH U⊃(W⊗V)⊗U=W⊗(V⊗U)
;id uniqueness
(assume |id u ∧id w ∧ length u=length w|)
(rw * (open id))
;(∀N.N<LENGTH U⊃NTH(U,N)=N)∧(∀N.N<LENGTH U⊃NTH(W,N)=N)∧LENGTH U=LENGTH W
(ue ((u.u)(v.w)) extensionality (open appl) *)
;U=W
(ci -3)
;ID(U)∧ID(W)∧LENGTH U=LENGTH W⊃U=W
;theorem 2(i):id implies perm
(proof idperm)
1. (trw |ID(U)⊃INTO(U)| (open id into))
;ID(U)⊃INTO(U)
(label p_i1)
;verification of ontoness is almost as trivial
2. (assume |id(u)|)(label p_i2)
3. (rw * (open id))
;∀N.N<LENGTH U⊃NTH(U,N)=N
(label p_i3)
4. (assume |n<length u|)
(label p_i4)
5. (derive |member(nth(u,n),u)| (* nthmember))
6. (derive |member(n,u)| (* p_i4 p_i3))
7. (ci p_i4)
;N<LENGTH U⊃MEMBER(N,U)
8. (derive |perm u| (p_i1 p_i2 *) (open perm onto))
9. (ci p_i2)
;ID(U)⊃PERM(U)
(label id_perm)
;theorem 2(ii):identity right
(proof identity)
1. (assume |id u∧length w=length u|)
2. (rw * (open id))
;(∀N.N<LENGTH U⊃NTH(U,N)=N)∧LENGTH W=LENGTH U
;labels: DEF_APPL_CONDITION
;∀U V.INTO(U)∧LENGTH U≤LENGTH V⊃DEF_APPL(V,U)
3. (ue ((u.u)(v.w))
def_appl_condition * (open lesseq into))
;DEF_APPL(W,U)
;deps: (1)
;labels: NTH_COMPOSE
1. (AXIOM |∀V U N.DEF_APPL(V,U)∧N<LENGTH U⊃NTH(V⊗U,N)=NTH(V,NTH(U,N))|)
4. (ue ((u.u)(v.w)(n.n)) nth_compose * (use -2 mode: exact))
;N<LENGTH U⊃NTH(W⊗U,N)=NTH(W,N)
;deps: (1)
;labels: EXTENSIONALITY
;∀U V.LENGTH U=LENGTH V∧(∀I.I<LENGTH U⊃APPL(U,I)=APPL(V,I))⊃U=V
5. (ue ((u.|w⊗u|)(v.w)) extensionality (open appl)
(use length_compose -2 * 1))
;W⊗U=W
;deps: (1)
6. (ci 1)
;ID(U)∧LENGTH W=LENGTH U⊃W⊗U=W
;theorem 2(iii):identity left
(proof identity_left)
1. (assume |id u∧perm w∧length w=length u|)
(label il_1)
2. (derive |def_appl(u,w)| (il_1 def_appl_condition1))
;deps: (IL_1)
(label il_2)
3. (rw il_1 (open perm onto into id))
;(∀N.N<LENGTH U⊃NTH(U,N)=N)∧
;(∀N.N<LENGTH W⊃NATNUM(NTH(W,N))∧NTH(W,N)<LENGTH W)∧
;(∀N.N<LENGTH U⊃MEMBER(N,W))∧LENGTH W=LENGTH U
;deps: (IL_1)
4. (ue ((v.u)(u.w)) nth_compose il_2 *)
;∀N.N<LENGTH U⊃NTH(U⊗W,N)=NTH(W,N)
;deps: (IL_1)
5. (ue ((u.|u⊗w|)(v.w)) extensionality
(sortcomp il_1 il_2 length_compose *) (open appl))
;U⊗W=W
;deps: (IL_1)
6. (ci il_1)
;ID(U)∧PERM(W)∧LENGTH W=LENGTH U⊃U⊗W=W
;lemma inv implies into
(proof inv_into)
1. (assume |perm(u)|)
(label ii1)
2. (assume |inv(v,u)|)
(label ii2)
3. (assume |length v=length u|)
(label ii3)
4. (rw ii1 (open perm into onto) )
(label ii4)
;(∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U)∧(∀N.N<LENGTH U⊃MEMBER(N,U))
5. (rw ii2 (open inv))
(label ii5)
;∀N.N<LENGTH V⊃NTH(V,N)=FSTPOSITION(U,N)
6. (assume |m<length v|)
(label ii6)
7. (derive |NTH(V,M)=FSTPOSITION(U,M)| (ii5 ii6))(label ii7)
8. (rw ii6 (use ii3 mode: exact))
;M<LENGTH U
9. (derive |member(m,u)| (* ii4))
;MEMBER(M,U)
10. (trw |natnum fstposition(u,m)∧fstposition(u,m)<length u|
(use pos_length * mode: always) (use posfacts ue: ((u.u)(y.m)) ))
;NATNUM(FSTPOSITION(U,M))∧FSTPOSITION(U,M)<LENGTH U
11. (rw * (use ii3 ii7 mode: exact direction: reverse))
;NATNUM(NTH(V,M))∧NTH(V,M)<LENGTH V
;deps: (II1 II2 II3 II6)
12. (ci ii6)
;M<LENGTH V⊃NATNUM(NTH(V,M))∧NTH(V,M)<LENGTH V
13. (trw |into v| (open into) *)
;INTO(V)
;deps: (II1 II2 II3)
14. (ci (ii1 ii2 ii3))
;PERM(U)∧INV(V,U)∧LENGTH V=LENGTH U⊃INTO(V)
;theorem 3(i):inv implies perm
(proof inv_onto)
1. (assume |perm u|)
(label io1)
2. (assume |inv(v,u)|)
(label io2)
3. (assume |length v=length u|)
(label io3)
4. (rw io1 (open perm into onto) )
;(∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U)∧
;(∀N.N<LENGTH U⊃MEMBER(N,U))
(label io4)
5. (rw io2 (open inv))
;∀N.N<LENGTH V⊃NTH(V,N)=FSTPOSITION(U,N)
(label io5)
6. (derive |∀n.n<length u⊃fstposition(u,nth(u,n))=n|
(fstposition_nth perm_injectivity uniqueness_injectivity io1 io4))
(label io6)
7. (assume |n<length v|)
(label io7)
8. (rw * (use io3 mode: exact))
;N<LENGTH U
(label io8)
;deps: (IO3 IO7)
9. (derive |NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH V| (io3 io4 io8))
;deps: (IO1 IO3 IO7)
(label io9)
;so we can use the fact that V is the inverse of U...
10. (trw |NTH(V,NTH(U,N))=FSTPOSITION(U,NTH(U,N))|(io5 *))
;NTH(V,NTH(U,N))=FSTPOSITION(U,NTH(U,N))
;deps: (IO1 IO2 IO3 IO7)
(label io10)
;...the lemma fstposition_nth
11. (rw * (use io6 io8 mode: exact))
;NTH(V,NTH(U,N))=N
(label io11)
;deps: (IO1 IO2 IO3 IO7)
;...the lemma nthmember
12. (trw |member(nth(v,nth(u,n)),v)| (nthmember io9))
;MEMBER(NTH(V,NTH(U,N)),V)
;deps: (IO1 IO3 IO7)
13. (rw * (use io11 mode: exact))
;MEMBER(N,V)
;deps: (IO1 IO2 IO3 IO7)
;...and obtain the second condition for ontoness
14. (ci io7)
;N<LENGTH V⊃MEMBER(N,V)
;deps: (IO1 IO2 IO3)
15. (derive |into v| (inv_into io1 io2 io3))
;deps: (IO1 IO2 IO3)
16. (trw |perm v| (open perm onto) -2 *)
;PERM(V)
;deps: (IO1 IO2 IO3)
17. (ci (IO1 IO2 IO3))
;PERM(U)∧INV(V,U)∧LENGTH V=LENGTH U⊃PERM(V)
;theorem 3(ii):inverse_right;
(proof inverse_right)
1. (assume |perm w∧inv(u,w)∧length u=length w|)
(label cir1)
2. (rw cir1 (open perm onto inv))
;INTO(W)∧(∀N.N<LENGTH U⊃MEMBER(N,W))∧
;(∀N.N<LENGTH U⊃NTH(U,N)=FSTPOSITION(W,N))∧
;LENGTH U=LENGTH W
;deps: (CIR1)
(label cir2)
3. (derive |perm u|(inv_perm cir1))
;deps: (CIR1)
4. (ue ((v.w)(u.u)) def_appl_condition1 (cir1 *))
;DEF_APPL(W,U)
;deps: (CIR1)
(label cir3)
;so we can apply nth_compose...
5. (ue ((v.w)(u.u)) nth_compose cir3 (use cir2 mode: always))
;∀N.N<LENGTH W⊃NTH(W⊗U,N)=NTH(W,FSTPOSITION(W,N))
;deps: (CIR1)
;...nth_fstposition...
;labels: NTH_FSTPOSITION
;∀U N.MEMBER(N,U)⊃NTH(U,FSTPOSITION(U,N))=N
6. (ue (u w) nth_fstposition cir2)
;∀N.MEMBER(N,W)⊃NTH(W,FSTPOSITION(W,N))=N
;deps: (CIR1)
7. (derive |∀n.n<length w⊃nth(w,fstposition(w,n))=n| (nth_fstposition cir2))
;deps: (CIR1)
8. (rw -2 (use * mode: exact))
;∀N.N<LENGTH W⊃NTH(W⊗U,N)=N
;deps: (CIR1)
9. (trw |id(w⊗u)| * (open id)
(use cir2 cir3 length_compose perm_compose mode: always))
;ID(W⊗U)
;deps: (CIR1)
10. (ci cir1)
;PERM(W)∧INV(U,W)∧LENGTH U=LENGTH W⊃ID(W⊗U)
;;;;;;;;;;;;
;facts used:
;labels: LENGTH_COMPOSE
;(AXIOM |∀W U.DEF_APPL(W,U)⊃LENGTH (W⊗U)=LENGTH U|)
;labels: NTH_FSTPOSITION
;(AXIOM |∀U N.MEMBER(N,U)⊃NTH(U,FSTPOSITION(U,N))=N|)
;labels: NTH_COMPOSE
;(AXIOM |∀V U N.DEF_APPL(V,U)∧N<LENGTH U⊃NTH(V⊗U,N)=NTH(V,NTH(U,N))|)
(show def_appl_condition1)
;labels: DEF_APPL_CONDITION1
;∀U V.PERM(U)∧LENGTH U=LENGTH V⊃DEF_APPL(V,U)
;theorem 3(iii):inverse left;
(proof inv_left)
1. (assume |perm w|)
(label cil0)
2. (assume |inv(u,w)|)
(label cil1)
3. (assume |length u=length w|)
(label cil2)
4. (rw cil0 (open perm onto into))
;(∀N.N<LENGTH W⊃NATNUM(NTH(W,N))∧NTH(W,N)<LENGTH W)∧
;(∀N.N<LENGTH W⊃MEMBER(N,W))
(label cil3)
;deps: (CIL0)
5. (rw cil1 (open inv))
;(∀N.N<LENGTH U⊃NTH(U,N)=FSTPOSITION(W,N))
(label cil4)
;deps: (CIL1)
;two conditions verified
6. (ue ((v.u)(u.w)) def_appl_condition1 cil0 cil2)
;DEF_APPL(U,W)
(label cil5)
;deps: (CIL0 CIL2)
7. (derive |∀n.n<length w⊃fstposition(w,nth(w,n))=n|
(fstposition_nth perm_injectivity uniqueness_injectivity cil0 cil3))
(label cil6)
;deps: (CIL0)
8. (assume |n<length w|)
(label cil7)
9. (ue (n |nth(w,n)|) cil4 cil3 cil7 (use cil2 mode: exact))
;NTH(U,NTH(W,N))=FSTPOSITION(W,NTH(W,N))
;deps: (CIL0 CIL1 CIL2 CIL7)
10. (rw * (use cil6 cil7 mode: always))
;NTH(U,NTH(W,N))=N
;deps: (CIL0 CIL1 CIL2 CIL7)
11. (ci cil7)
;N<LENGTH W⊃NTH(U,NTH(W,N))=N
;deps: (CIL0 CIL1 CIL2)
12. (ue ((v.u)(u.w)) nth_compose cil5 (use * mode: always))
;∀N.N<LENGTH W⊃NTH(U⊗W,N)=N
;deps: (CIL0 CIL1 CIL2)
13. (trw |id(u⊗w)| (open id) * length_compose cil5)
;ID(U⊗W)
;deps: (CIL0 CIL1 CIL2)
14. (ci (cil0 cil1 cil2))
;PERM(W)∧INV(U,W)∧LENGTH U=LENGTH W⊃ID(U⊗W)
;;;;;;;;;
;labels: DEF_APPL_CONDITION1
;∀U V.PERM(U)∧LENGTH U=LENGTH V⊃DEF_APPL(V,U)
;labels: NTH_COMPOSE
;∀V U N.DEF_APPL(V,U)∧N<LENGTH U⊃NTH(V⊗U,N)=NTH(V,NTH(U,N))
;labels: FSTPOSITION_NTH
;∀U N.UNIQUENESS(U)∧MEMBER(N,U)⊃FSTPOSITION(U,NTH(U,N))=N
;labels: LENGTH_COMPOSE
;∀W U.DEF_APPL(W,U)⊃LENGTH (W⊗U)=LENGTH U
;labels: LENGTH_COMPOSE
;∀W U.DEF_APPL(W,U)⊃LENGTH (W⊗U)=LENGTH U
;application: sorts of the other functions
(unlabel simpinfo permf#9)
(ue (a |λn.∀m.listp ident1(m,n)|) proof_by_induction (open ident1))
;∀N M.LISTP IDENT1(M,N)
(trw |∀n.listp ident(n)| (open ident) *)
;∀N.LISTP IDENT(N)
(ue (a |λn.∀i.listp invers1(u,i,n)|) proof_by_induction (open invers1) posfacts)
;∀N I.LISTP INVERS1(U,I,N)
(trw |listp inverse(u)| (open inverse) *)
;LISTP INVERSE(U)
;length ident and lengthinverse
(ue (a |λn.∀m.length ident1(m,n)=n|) proof_by_induction (open ident1))
;∀N M.LENGTH (IDENT1(M,N))=N
;lemma lengthinverse
(proof lengthinverse)
1. (assume |perm(u)|)
(label li1)
2. (rw li1 (open perm onto into))
;(∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U)∧(∀N.N<LENGTH U⊃MEMBER(N,U))
(label li2)
3. (ue ((u.|u|) (y.|n|)) posfacts)
;(NULL FSTPOSITION(U,N)⊃¬MEMBER(N,U))∧(MEMBER(N,U)⊃NATNUM(FSTPOSITION(U,N)))
4. (derive |n<length u⊃¬null fstposition(u,n)| (3 li2))
(label li3)
5. (ue ((m.|n|) (n.|length u|)) minusfact11
((part 1 (use less_lesseqsucc mode: exact))))
;N'≤LENGTH U⊃LENGTH U-N'<LENGTH U
6. (derive |n'≤length u⊃¬null fstposition(u,length u-n')| (5 li3))
(label li4)
7. (trw |n'≤length u⊃(length u-n')'=length u-n|
((use minusfact10)
(use less_lesseqsucc mode: exact direction: reverse)))
;N'≤LENGTH U⊃(LENGTH U-N')'=LENGTH U-N
8. (ue ((a.|λn.n≤length u⊃length (invers1(u,length u-n,n))=n|))
proof_by_induction
((open invers1) (use succ_lesseq_lesseq) (use 7) (use li4)))
;∀N.N≤LENGTH U⊃LENGTH (INVERS1(U,LENGTH U-N,N))=N
9. (ue (n |length u|) * (open lesseq))
;LENGTH (INVERS1(U,0,LENGTH U))=LENGTH U
10. (trw |length inverse(u)=length u| (open inverse) *)
;LENGTH (INVERSE(U))=LENGTH U
;deps: (LI1)
11. (ci li1)
;PERM(U)⊃LENGTH (INVERSE(U))=LENGTH U
;id main
(proof id_main)
1. (assume |nthcdr(ident(m),n)=n.ident1(n',m-n')|)
2. (trw |cdr nthcdr(ident(m),n)| (use * mode: exact))
;CDR NTHCDR(IDENT(M),N)=IDENT1(N',M-N')
3. (ci -2)
;NTHCDR(IDENT(M),N)=N.IDENT1(N',M-N')⊃
;CDR NTHCDR(IDENT(M),N)=IDENT1(N',M-N')
4. (ue (a |λn.n<m⊃nthcdr(ident(m),n)=ident1(n,m-n)|) proof_by_induction
(open ident1)
(part 1#2#1#1 (use minusfact10 succ_less_less mode: exact))
(part 1#2#1 (use cdr_nthcdr mode: exact direction: reverse))
(use * succ_less_less mode: exact)
(part 1#1 (open minus ident)))
;∀N.N<M⊃NTHCDR(IDENT(M),N)=IDENT1(N,M-N)
5. (rw * (use minusfact10 mode: exact))
;∀N.N<M⊃NTHCDR(IDENT(M),N)=IDENT1(N,(M-N')')
;labels: CAR_NTHCDR
;∀U N.N<LENGTH U⊃CAR NTHCDR(U,N)=NTH(U,N)
6. (ue ((u.|ident m|)(n.n)) car_nthcdr (use * mode: always))
;N<M⊃N=NTH(IDENT(M),N)
;the following doesn't work:
;(ue (a |λn.n<m⊃nthcdr(ident(m),n)=ident1(n,m-n)|) proof_by_induction
; (open ident1)
; (part 1#2#1#1 (use minusfact10 succ_less_less mode: exact))
; (part 1#2#1 (use cdr_nthcdr mode: exact direction: reverse))
; (use succ_less_less mode: always)
; (part 1#1 (open minus ident)))
;(∀N.(N<M⊃NTHCDR(IDENT(M),N)=N.IDENT1(N',M-N'))⊃
; (N'<M⊃CDR NTHCDR(IDENT(M),N)=IDENT1(N',M-N')))⊃
;(∀N.N<M⊃NTHCDR(IDENT(M),N)=IDENT1(N,M-N))
;theorem 2 as corollary
(proof ident_corollary)
1. (trw |∀n.id(ident(n))| (open id) id_main ident_length)
(label id_ident)
;∀N.ID(IDENT(N))
;theorem 2 (i)
2. (trw |∀n.perm(ident n)| (id_perm id_ident))
;∀N.PERM(IDENT(N))
(label perm_ident)
;theorem 2 (ii)
3. (trw |∀u.u⊗ident(length u)=u| (id_right id_ident ident_length))
;∀U.U⊗IDENT(LENGTH U)=U
(label identity_right_theorem)
;theorem 2 (iii)
4. (trw |∀u.perm(u)⊃u=ident(length u)⊗u| (id_left id_ident ident_length))
;∀U.PERM(U)⊃U=IDENT(LENGTH U)⊗U
(label identity_left_theorem)
;inv main
(proof inverse_main)
1. (assume |perm u|)
(label inv_main1)
2. (rw inv_main1 (open perm onto))
;INTO(U)∧(∀N.N<LENGTH U⊃MEMBER(N,U))
(label inv_main2)
3. (ue ((u.u)(y.n)) posfacts)
;(NULL FSTPOSITION(U,N)⊃¬MEMBER(N,U))∧(MEMBER(N,U)⊃NATNUM(FSTPOSITION(U,N)))
4. (derive |n<length u⊃¬null fstposition(u,n)| (inv_main2 *))
(label inv_main3)
5. (assume |nthcdr(inverse(u),n)=fstposition(u,n).invers1(u,n',length u-n')|)
6. (trw |cdr nthcdr(inverse(u),n)| (use * mode: exact))
;CDR NTHCDR(INVERSE(U),N)=INVERS1(U,N',LENGTH U-N')
7. (ci -2)
;NTHCDR(INVERSE(U),N)=FSTPOSITION(U,N).INVERS1(U,N',LENGTH U-N')⊃
;CDR NTHCDR(INVERSE(U),N)=INVERS1(U,N',LENGTH U-N')
8. (ue (a |λn.n<length u⊃nthcdr(inverse(u),n)=invers1(u,n,length u-n)|)
proof_by_induction (open invers1)
(part 1#2#1#1 (use minusfact10 succ_less_less mode: exact))
(part 1#2#1 (use cdr_nthcdr mode: exact direction: reverse)
(use inv_main3 mode: exact))
(use * succ_less_less mode: exact)
(part 1#1(open inverse minus)))
;∀N.N<LENGTH U⊃NTHCDR(INVERSE(U),N)=INVERS1(U,N,LENGTH U-N)
;deps: (INV_MAIN1)
9. (rw * (use minusfact10 mode: exact) (open invers1)
(use inv_main3 mode: always))
;∀N.N<LENGTH U⊃
;NTHCDR(INVERSE(U),N)=FSTPOSITION(U,N).INVERS1(U,N',LENGTH U-N')
;deps: (INV_MAIN1)
;labels: CAR_NTHCDR
;∀U N.N<LENGTH U⊃CAR NTHCDR(U,N)=NTH(U,N)
10. (ue ((u.|inverse(u)|)(n.n)) car_nthcdr
(use * lengthinverse inv_main1 mode: always))
;N<LENGTH U⊃FSTPOSITION(U,N)=NTH(INVERSE(U),N)
;deps: (INV_MAIN1)
11. (ci inv_main1)
;PERM(U)⊃(N<LENGTH U⊃FSTPOSITION(U,N)=NTH(INVERSE(U),N))
;theorem 3 as corollary
(proof inverse_corollary)
1. (trw |∀u.perm u⊃inv(inverse u,u)| (open inv) inv_main lengthinverse)
;∀U.PERM(U)⊃INV(INVERSE(U),U)
(label inv_inverse)
;theorem 3(i)
2. (trw |∀u.perm(u)⊃perm(inverse u)| (inv_perm inv_inverse lengthinverse))
;∀U.PERM(U)⊃PERM(INVERSE(U))
(label perm_inverse)
;theorem 3(ii)
;two conditions verified
3. (assume |perm u|)
(label assumption)
4. (derive |perm inverse(u) ∧ length inverse(u) = length u|
(* perm_inverse lengthinverse))
5. (ue ((u.|inverse u|)(v.u)) def_appl_condition1 *)
;DEF_APPL(U,INVERSE(U))
6. (ci -3)
;PERM(U)⊃DEF_APPL(U,INVERSE(U))
(label def_appl_inv_condition1)
7. (trw |perm u⊃length(u⊗(inverse u))=length u|
(length_compose def_appl_inv_condition1 lengthinverse))
;PERM(U)⊃LENGTH (U⊗INVERSE(U))=LENGTH U
(label length_inv_condition1)
;apply id uniqueness
8. (trw |∀u.perm(u)⊃id(u⊗inverse u)|
(inv_right lengthinverse inv_inverse))
;∀U.PERM(U)⊃ID(U⊗INVERSE(U))
9. (ue ((u.|u⊗inverse u|)(w.|ident(length u)|)) id_uniqueness
(assumption def_appl_inv_condition1
* id_ident ident_length length_inv_condition1))
;U⊗INVERSE(U)=IDENT(LENGTH U)
;deps: (ASSUMPTION)
10. (ci assumption)
;PERM(U)⊃U⊗INVERSE(U)=IDENT(LENGTH U)
(label compose_inverse_right)
;theorem 3(iii)
11. (ue ((u.u)(v.|inverse u|)) def_appl_condition1 perm_inverse lengthinverse)
;PERM(U)⊃DEF_APPL(INVERSE(U),U)
(label def_appl_inv_condition2)
12. (derive |perm u⊃length((inverse u)⊗u)=length u| (length_compose *))
(label length_inv_condition2)
13. (trw |∀u.perm(u)⊃id(inverse(u)⊗u)|
(inv_left lengthinverse inv_inverse))
;∀U.PERM(U)⊃ID(INVERSE(U)⊗U)
14. (ue ((u.|inverse(u)⊗u|)(w.|ident(length u)|)) id_uniqueness
(assumption def_appl_inv_condition2
* id_ident ident_length length_inv_condition2))
;INVERSE(U)⊗U=IDENT(LENGTH U)
;deps: (ASSUMPTION)
15. (ci assumption)
;PERM(U)⊃INVERSE(U)⊗U=IDENT(LENGTH U)
(label compose_inverse_left)